#include <stdio.h>
#include <stdlib.h>
#include <string.h>
#include "klee_change_macros.h"
#include "klee_change_functions.h"
int lib(int x) {
	return x % klee_change(5,6);
}

int client(int x){
	x = x*5*6;
	if (lib(x)==0){
		return 1;
	}else{
		return 0;
	}
}

int main(int argc, char *argv[]) {
  int x= argv[1][0] - '0';
  return client(x);
}
